A, B, C, D:Realizer. A  C  B  D  C || D  A || B 

latex

Definitions	T, {T}, SQType(T), P  Q, True, , ff, tt, Rnone?(x1), if b then t else f fi , Y, P & Q, Rplus-right(x1), Rplus-left(x1), Rplus?(x1), A || B, A  B, i  j , False, A, A  B, t  T, P  Q, x:A. B(x), P  Q, Unit, , , Dec(P), ,
Lemmas	true wf, squash wf, bool sq, bool cases, Rplus wf, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, Rplus-right wf, Rplus-left wf, R-size-decreases, Rplus-implies, ge wf, nat properties, Rplus? wf, decidable assert, es realizer wf, nat plus wf, le wf, R-sub wf, R-compat wf, R-size wf, nat wf